Presentation: Basics of Functional K

Slide 1: Introduction to K and Its Basics

Slide 2: The First K Program

Slide 3: Running K Programs

Slide 4: Productions, Constructors, and Functions

Slide 5: Alternative K Definitions

Slide 6: Rules, Matching, and Variables

Slide 7: Extended Exercise 1

Slide 8: Extended Exercise 2

Slide 9: Summary of Key Concepts

Slide 10: BNF Syntax and Parser Generation

Understanding K’s Parsing Mechanisms and Syntax Definitions

BNF Notation: An Overview

1. Definition of BNF:

2. Purpose:

3. Components of BNF:
BNF consists of several key components, which include:

4. Example of BNF:
Here’s a simple example of BNF to define basic arithmetic expressions:

<expression> ::= <term> | <term> '+' <expression> | <term> '-' <expression>
<term> ::= <factor> | <factor> '*' <term> | <factor> '/' <term>
<factor> ::= <number> | '(' <expression> ')'
<number> ::= <digit> | <digit> <number>
<digit> ::= '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'

Explanation of the Example:

5. Advantages of BNF:

6. Variants of BNF:

Slide 11: Learning Objectives

Slide 12: K’s Parsing Approach

Slide 13: BNF Productions in K

module LESSON-03-A
  syntax Boolean ::= "true" | "false"
                   | "!" Boolean [function]
                   | Boolean "&&" Boolean [function]
                   | Boolean "^" Boolean [function]
                   | Boolean "||" Boolean [function]
endmodule

Slide 14: BNF Notation

- K uses BNF to distinguish between:

Example:

syntax Color ::= "Yellow" "(" ")" | "Blue" "(" ")"

Slide 15: Parsing Example with kast

inj{SortBoolean{}, SortKItem{}}(
  Lbl'UndsAnd-And-UndsUnds'LESSON-03-A'Unds'Boolean'Unds'Boolean'Unds'Boolean{}(
    Lbltrue'Unds'LESSON-03-A'Unds'Boolean{}(),
    Lblfalse'Unds'LESSON-03-A'Unds'Boolean{}()
  )
)

Slide 16: Ambiguities in Parsing

Slide 17: Handling Brackets in K

module LESSON-03-D
  syntax Boolean ::= "true" | "false"
                   | "(" Boolean ")" [bracket]
                   | "!" Boolean [function]
                   | Boolean "&&" Boolean [function]
                   | Boolean "||" Boolean [function]
endmodule

Slide 18: Token Definitions in K

Slide 19: Disambiguating Parses

  1. Priority Blocks:

    • Used to specify the precedence of different operators.
    • Operators with higher precedence (tighter binding) will not allow lower precedence (looser binding) operators to appear as direct children in their AST.
    • Example: In the expression true && false || false, && has higher precedence than ||, resulting in the AST being (true && false) || false.

  2. Associativity:

    • Defines how operators of the same precedence are parsed.
    • Left-associative operators can’t be the direct rightmost child of themselves, while right-associative operators can’t be the direct leftmost child.
    • Example: The expression true && false && false is parsed as (true && false) && false because && is left-associative.

  3. Explicit Priority and Associativity Declarations:

    • Allows grouping of productions across different sections of the grammar.
    • Use of group(_) for organizing related productions and applying priority and associativity to those groups.

  4. Prefer/Avoid Attributes:

    • Used to resolve ambiguities directly by instructing the parser to prefer one parse over another.
    • avoid attribute can be added to a production to disallow it in the event of ambiguity.

Slide 20: Modules, Imports, and Requires in K Definitions

Slide 21: K’s Outer Syntax

Slide 22: Basic Module Syntax

Slide 23 : Imports

Slide 24 : Parsing with Multiple Modules

Slide 25: Main Syntax and Semantics Modules

Slide 26: Splitting a Definition into Multiple Files

Slide 27: Putting It All Together

Slide 28: Solidity File: SimpleArithmetic.sol

This smart contract provides basic arithmetic operations similar to the definitions we created in K.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract SimpleArithmetic {
    // Function to add two integers
    function add(int a, int b) public pure returns (int) {
        return a + b;
    }

    // Function to subtract two integers
    function subtract(int a, int b) public pure returns (int) {
        return a - b;
    }

    // Function to multiply two integers
    function multiply(int a, int b) public pure returns (int) {
        return a * b;
    }

    // Function to divide two integers
    function divide(int a, int b) public pure returns (int) {
        require(b != 0, "Division by zero");
        return a / b;
    }

    // Function to evaluate a boolean expression
    function evaluate(bool a, bool b) public pure returns (bool) {
        return a && b; // Logical AND
    }

    // Function to evaluate NOT
    function negate(bool a) public pure returns (bool) {
        return !a; // Logical NOT
    }
}

Explanation of SimpleArithmetic.sol

  1. Contract Declaration: contract SimpleArithmetic defines a new Solidity smart contract named SimpleArithmetic.

  2. Function Definitions:

    • Each function performs a basic arithmetic operation (add, subtract, multiply, divide).
    • The divide function includes a check to prevent division by zero using require.

  3. Boolean Operations:

    • The evaluate function implements a logical AND operation.
    • The negate function implements a logical NOT operation.

K Framework Testing Definitions

1. File: solidity-tests.k

This file will contain the necessary K definitions to specify properties for testing the Solidity contract.

module SOLIDITY-TESTS
  // Importing necessary modules for Boolean and Arithmetic operations
  requires "booleans.k"
  requires "arithmetic.k"

  // Syntax for Solidity function calls and parameters
  syntax FunctionCall ::= "add" "(" Int "," Int ")" [function]
  syntax FunctionCall ::= "subtract" "(" Int "," Int ")" [function]
  syntax FunctionCall ::= "multiply" "(" Int "," Int ")" [function]
  syntax FunctionCall ::= "divide" "(" Int "," Int ")" [function]
  syntax FunctionCall ::= "evaluate" "(" Boolean "," Boolean ")" [function]
  syntax FunctionCall ::= "negate" "(" Boolean ")" [function]

  // Define evaluation rules for testing the smart contract functions
  rule evalExpr(add(X, Y)) => X + Y
  rule evalExpr(subtract(X, Y)) => X - Y
  rule evalExpr(multiply(X, Y)) => X * Y
  rule evalExpr(divide(X, Y)) => Y == 0 => "Division by zero" // Handle division by zero case
  rule evalExpr(divide(X, Y)) => X / Y
  rule evalExpr(evaluate(A, B)) => A && B
  rule evalExpr(negate(A)) => not A

endmodule

Explanation of solidity-tests.k

2. File: run_tests.sh

You can use a simple shell script to compile and run the tests.

#!/bin/bash

# Compile the Solidity contract
echo "Compiling the Solidity contract..."
solc --bin --abi SimpleArithmetic.sol -o build/

# Run the K tests
echo "Running K tests..."
kompile solidity-tests.k --main-module SOLIDITY-TESTS

# Execute the K test with krun
krun result.k

# Add any additional commands to verify the output as necessary

Running the Tests

  1. Compile the Solidity Contract:

    • Use the solc command to compile the SimpleArithmetic.sol contract. This generates binary and ABI files in the build/ directory.

  2. Run the K Tests:

    • Compile the K definitions using kompile.
    • Run the test using krun.

  3. Output Verification:

    • Depending on the logic you want to validate, check the output of the K tests against the expected results from the Solidity functions.

Summary

In this setup, we created a simple Solidity smart contract that performs arithmetic and Boolean operations. We also defined a corresponding K framework for testing the smart contract’s functionality by specifying properties of the operations we implemented.

By executing the K tests, you can ensure that the operations in the Solidity contract behave as expected, and any discrepancies can be identified and addressed. This approach effectively combines smart contract development and formal verification through the K framework.